\begin{tabbing}
$\forall$$D$:Dsys, $L$:Id List.
\\[0ex]($\forall$$i$:Id. ($i$ $\in$ $L$) $\vee$ ma{-}is{-}empty(M($i$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$:Id. Feasible(M($i$)))
\\[0ex]$\Rightarrow$ (\=$\forall$$i$$\in$$L$.\+
\\[0ex]$\forall$${\it ltg}$$\in$ma{-}outlinks(M($i$);$i$).
\\[0ex](destination(1of(${\it ltg}$)) $\in$ $L$)
\\[0ex]$\Rightarrow$ interface{-}check($D$;1of(${\it ltg}$);1of(2of(${\it ltg}$));2of(2of(${\it ltg}$))))
\-\\[0ex]$\Rightarrow$ Feasible($D$)
\end{tabbing}